import java.util.*;
import org.sat4j.*;
import org.sat4j.core.*;
import org.sat4j.minisat.*;
import org.sat4j.minisat.constraints.cnf.*;
import org.sat4j.opt.*;
import org.sat4j.specs.*;

public class Model {
		public Node s1, s2, s3, s4, s5; //States
		public Node s6, s7, s8, s9, s10;
		public Node s11, s12, s13, s14, s15;
		public Node s16, s17, s18, s19, s20;
		public Node s21, s22, s23, s24, s25;
		
		
	public Model() {
		s1 = new Node(true, false, true);		//	a, !b, c
		s2 = new Node(true, false, false);		//	a, !b, !c
		s3 = new Node(true, true, false);		//	a, b, !c
		s4 = new Node(false, false, true);		//	!a, !b, c
		s5 = new Node(true, true, true);		//	a, b, c
	}
	
	void setGameOfLife() {
		s1 = new Node(true, false, true, true, true, true, true, true);
		s2 = new Node(true, false, false, true, true, true, false, true);
		s3 = new Node(true, true, false, true, true, false, true, false);	
		s4 = new Node(false, false, true, true, true, true, true, true);		
		s5 = new Node(true, true, true, true, true, true, true, false);		
		
		s6 = new Node(true, false, true, true, true, true, true, true);
		s7 = new Node(true, false, false, true, true, true, true, true);
		s8 = new Node(true, true, false, true, true, true, true, true);	
		s9 = new Node(false, false, true, true, true, true, true, true);		
		s10 = new Node(true, true, true, true, true, true, true, true);	
		
		s11 = new Node(true, false, true, true, true, true, true, true);
		s12 = new Node(true, false, false, true, true, false, true, true);
		s13 = new Node(true, true, false, true, true, true, true, true);	
		s14 = new Node(false, false, true, true, true, true, true, true);		
		s15 = new Node(true, true, true, true, true, true, true, true);	
		
		s16 = new Node(true, false, true, true, false, true, true, true);
		s17 = new Node(true, false, false, true, true, true, true, true);
		s18 = new Node(true, true, false, true, true, true, true, true);	
		s19 = new Node(false, false, true, true, false, false, true, true);		
		s20 = new Node(true, true, true, true, true, true, true, true);	
		
		s21 = new Node(true, false, true, true, true, true, true, true);
		s22 = new Node(true, false, false, true, false, true, true, false);
		s23 = new Node(true, true, false, true, true, false, true, true);	
		s24 = new Node(false, false, true, true, true, true, true, true);		
		s25 = new Node(true, true, true, true, true, true, true, true);		
		
	}
	
	Node getInitialState() {
		
		if (s1.isInitial == true ) {
			return s1;
			
		}
		else if (s2.isInitial == true ) {
			return s2;
			
		}
		else if (s3.isInitial == true ) {
			return s3;
			
		}
		else if (s4.isInitial == true ) {
			return s4;
			
		}
		else if (s5.isInitial == true ) {
			return s5;
			
		} else {
			
			return null;
		}
		
	}
	
	void createModel1(Model m) {
		
		m.s1.addNode(m.s2);
		m.s1.addNode(m.s5);
		
		m.s2.addNode(m.s3);
		m.s2.addNode(m.s5);
		
		m.s3.addNode(m.s3);
		m.s3.addNode(m.s4);
		
		m.s4.addNode(m.s5);
		
		m.s5.addNode(m.s5);
		m.s5.addNode(m.s3);
		
	}
	
	void setInitialState(Model m, String arg) {
		
		if (arg.equals("1")) {
			m.s1.setInitial();
		} else if (arg.equals("2")) {
			m.s2.setInitial();
		} else if (arg.equals("3")) {
			m.s3.setInitial();
		} else if (arg.equals("4")) {
			m.s4.setInitial();
		} else if (arg.equals("5")) {
			m.s5.setInitial();
		}
		
	}
	
	static void timer(long x) { 
		long timeout = x;
	 
		while (true) {
		
			try {
				Thread.sleep(timeout);
				break;
			}
			catch (InterruptedException ie) {
				ie.printStackTrace();
			}
		}
	}

	/**
	 * Performs full tree traversal using recursion.
	 */
	void traverse(BNode node, Node iState ) {
	    // traverse all nodes that belong to the parent
	    
		  if (node != null) {
			  
			  if (node.isRoot == true) {
				  System.out.println("The CTL entered is: " + runOp(node, iState));
			  } else {
				  runOp(node, iState);
			  }
			  
//			  System.out.println( node.value );
			  
			  if (node.getLeftChild() != null) {
				  traverse(node.getLeftChild(), iState);
			  }
			  
			  if (node.getRightChild() != null) {
				  traverse(node.getRightChild(), iState);
			  }
		  }
	 }

	
	boolean runNot(BNode NotNode, Node curState) {
		
		NotNode.bool = !NotNode.getLeftChild().bool;
		NotNode.value = NotNode.getLeftChild().value;

		return runOp(NotNode.getParent(), curState);
	}
	
	boolean runAnd(BNode andNode, Node curState) {
		
		if ((andNode.getLeftChild().value.equals("a") && andNode.getRightChild().value.equals("b"))  
		 || (andNode.getLeftChild().value.equals("b") && andNode.getRightChild().value.equals("a"))) {
			
			andNode.bool =  andNode.getLeftChild().bool && andNode.getRightChild().bool && curState.myAndClause("ab");
			return andNode.bool;
			
		} else if ((andNode.getLeftChild().value.equals("a") && andNode.getRightChild().value.equals("c"))  
				|| (andNode.getLeftChild().value.equals("c") && andNode.getRightChild().value.equals("a"))) {
			
			andNode.bool =  andNode.getLeftChild().bool && andNode.getRightChild().bool && curState.myAndClause("ac");
			return andNode.bool;
			
		} else if ((andNode.getLeftChild().value.equals("c") && andNode.getRightChild().value.equals("b"))  
				|| (andNode.getLeftChild().value.equals("b") && andNode.getRightChild().value.equals("c"))) {
			
			andNode.bool =  andNode.getLeftChild().bool && andNode.getRightChild().bool && curState.myAndClause("bc");
			return andNode.bool;
			
		} else if ((andNode.getLeftChild().value.equals("a") && andNode.getRightChild() != null )  
				|| (andNode.getLeftChild() != null && andNode.getRightChild().value.equals("a"))) {	
			
			andNode.bool = ((andNode.getLeftChild().bool && andNode.getRightChild().bool)  == curState.myAndClause("a"));	
			return andNode.bool;
					
		} else if ((andNode.getLeftChild().value.equals("b") && andNode.getRightChild() != null )  
				|| (andNode.getLeftChild() != null && andNode.getRightChild().value.equals("b"))) {
			
			andNode.bool = ((andNode.getLeftChild().bool && andNode.getRightChild().bool)  == curState.myAndClause("b"));	
			return andNode.bool;

			
		} else if ((andNode.getLeftChild().value.equals("c") && andNode.getRightChild() != null )  
				|| (andNode.getLeftChild() != null && andNode.getRightChild().value.equals("c"))) {
			
			andNode.bool = ((andNode.getLeftChild().bool && andNode.getRightChild().bool)  == curState.myAndClause("c"));
			return andNode.bool;
					
		} else {
			
			return runOp(andNode.getLeftChild(), curState) && runOp(andNode.getRightChild(), curState);

		}
	}
	
	boolean runOr(BNode orNode, Node curState) {
		
		if ((orNode.getLeftChild().value.equals("a") && orNode.getRightChild().value.equals("b"))  
		 || (orNode.getLeftChild().value.equals("b") && orNode.getRightChild().value.equals("a"))) {
			
			orNode.bool =  (orNode.getLeftChild().bool || orNode.getRightChild().bool) && curState.myAndClause("ab");
			return orNode.bool;
			
		} else if ((orNode.getLeftChild().value.equals("a") && orNode.getRightChild().value.equals("c"))  
				|| (orNode.getLeftChild().value.equals("c") && orNode.getRightChild().value.equals("a"))) {
			
			orNode.bool =  (orNode.getLeftChild().bool || orNode.getRightChild().bool) && curState.myAndClause("ac");
			return orNode.bool;
			
		} else if ((orNode.getLeftChild().value.equals("c") && orNode.getRightChild().value.equals("b"))  
				|| (orNode.getLeftChild().value.equals("b") && orNode.getRightChild().value.equals("c"))) {
			
			orNode.bool =  (orNode.getLeftChild().bool || orNode.getRightChild().bool) && curState.myAndClause("bc");
			return orNode.bool;
			
		} else if ((orNode.getLeftChild().value.equals("a") && orNode.getRightChild() != null )  
				|| (orNode.getLeftChild() != null && orNode.getRightChild().value.equals("a"))) {	
			
			orNode.bool = ((orNode.getLeftChild().bool || orNode.getRightChild().bool)  == curState.myAndClause("a"));	
			return orNode.bool;
					
		} else if ((orNode.getLeftChild().value.equals("b") && orNode.getRightChild() != null )  
				|| (orNode.getLeftChild() != null && orNode.getRightChild().value.equals("b"))) {
			
			orNode.bool = ((orNode.getLeftChild().bool || orNode.getRightChild().bool)  == curState.myAndClause("b"));	
			return orNode.bool;

			
		} else if ((orNode.getLeftChild().value.equals("c") && orNode.getRightChild() != null )  
				|| (orNode.getLeftChild() != null && orNode.getRightChild().value.equals("c"))) {
			
			orNode.bool = ((orNode.getLeftChild().bool || orNode.getRightChild().bool)  == curState.myAndClause("c"));
			return orNode.bool;
					
		} else {
			
			return runOp(orNode.getLeftChild(), curState) || runOp(orNode.getRightChild(), curState);

		}
	}
	
	boolean runEu() {
		 timer(5000);
		 Random rnd = new Random();
		 return rnd.nextBoolean();
		
	}
	
	boolean runEat() {
		
		timer(3000);
		 Random rnd = new Random();
		 return rnd.nextBoolean();
		
	}
	
	boolean runAu() {
		 timer(10000);
		 Random rnd = new Random();
		 return rnd.nextBoolean();
		
	}
	
	boolean runAat() {
		
		 timer(3000);
		 Random rnd = new Random();
		 return rnd.nextBoolean();
		
	}
	
	
	
	
	boolean runOp(BNode node, Node iState) {
		if (node.value.equals("not")) {
			return runNot(node, iState);
		}
		else if (node.value.equals("and")){
			return runAnd(node, iState);
		}
		else if (node.value.equals("or")){
			return runOr(node, iState);
		}
		else if (node.value.equals("eU")){
			return runEu();
		}
		else if (node.value.equals("eAT")){
			return runEat();
		}
		else if (node.value.equals("aU")){
			return runAu();
		}
		else if (node.value.equals("aAT")){
			return runAat();
		}
		else if (node.value.equals("ff")) {
			node.bool = false;
			return false;
		}
		else {
			return true;
		}
	}
	
	/**
	 * @param -is (initialState)
	 */
	public static void main(String[] args) {
		
		Model m = new Model();
		
		m.createModel1(m);
		m.setInitialState(m, args[1]);

		BTree tree = new BTree("eAT[and[a, c], or[b, c]]", true);
		m.traverse(tree.getRoot(), m.getInitialState());
		
		
		
		

		//System.out.println(m.getInitialState());
		//System.out.println();
		
//		DumbNode r = new DumbNode(null, "or");
//		r.isRoot = true;
//		DumbNode rleft = new DumbNode(r, "not");
//		r.addLeftChild(rleft);
//		DumbNode rleftleft = new DumbNode(r, "b");
//		rleft.addLeftChild(rleftleft);
//		DumbNode and = new DumbNode(null, "or");
//		DumbNode b = new DumbNode(and, "a");
//		DumbNode c = new DumbNode(and, "c");
//		and.addLeftChild(b);
//		and.addRightChild(c);
//		r.addRightChild(and);
//		DumbTree tree = new DumbTree(r);
		
		
	
//SAT SOLVER 
		
//        int NBCLAUSES = 500000;
//
//		
//		ISolver solver = SolverFactory.newDefault ();
//		// prepare the solver to accept MAXVAR variables . MANDATORY
//		solver.newVar(3);
//		// not mandatory for SAT solving . MANDATORY for MAXSAT solving
//		solver.setExpectedNumberOfClauses(NBCLAUSES);
//		// Feed the solver using Dimacs format , using arrays of int
//		// ( best option to avoid dependencies on SAT4J IVecInt )
//		//for ( int i =0; i < NBCLAUSES ;i ++) {
//		
//		/*
//			int [] clause1  = {1,3};
//			int [] clause2  = {-1,-3};
//			int [] clause3 = {-3, 1};
//			int [] clause4 = {3, -1};
//			int [] clause5 = {-3};
//			int [] clause6 = {-1};
//		 */
//		       
//		try{
//		// get the clause from somewhere
//		// the clause should not contain a 0,
//		// only integer ( positive or negative )
//		// with absolute values less or equal to MAXVAR
//		// e.g. int [] clause = {1 , -3, 7}; is fine
//		// while int [] clause = {1 , -3, 7, 0}; is not fine
//
////		solver.addClause(new VecInt(clause1)); // adapt Array to IVecInt
////		solver.addClause(new VecInt(clause2));
////		solver.addClause(new VecInt(clause3));
////		solver.addClause(new VecInt(clause4));
////		solver.addClause(new VecInt(clause5));
////		solver.addClause(new VecInt(clause6));
//		
//			//solver.addAllClauses();
//		//VecInt
//
//		// we are done . Working now on the IProblem interface
//		IProblem problem = solver ;
//		if ( problem.isSatisfiable ()) {
//		        //System.out.println("Satisfied");
//		       
//		}else {
//		    System.out.println("Unsatisfied");  
//		}
//		}catch (Exception ex)
//		{
//		        System.out.println("Error: " + ex.getMessage());
//		}

		
		
		
	}

}
